0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 1 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 4263 ms)
↳10 BOUNDS(1, n^2)
gcd(x, y) → gcd2(x, y, 0)
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i))
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i))
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i)
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i))
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i)
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i)
if3(true, b3, x, y, i) → if4(b3, x, y, i)
if4(false, x, y, i) → gcd2(x, minus(y, x), i)
if4(true, x, y, i) → pair(result(x), neededIterations(i))
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
a → b
a → c
gcd(x, y) → gcd2(x, y, 0) [1]
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i)) [1]
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i)) [1]
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i) [1]
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i)) [1]
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i) [1]
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i) [1]
if3(true, b3, x, y, i) → if4(b3, x, y, i) [1]
if4(false, x, y, i) → gcd2(x, minus(y, x), i) [1]
if4(true, x, y, i) → pair(result(x), neededIterations(i)) [1]
inc(0) → 0 [1]
inc(s(i)) → s(inc(i)) [1]
le(s(x), 0) → false [1]
le(0, y) → true [1]
le(s(x), s(y)) → le(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
a → b [1]
a → c [1]
gcd(x, y) → gcd2(x, y, 0) [1]
gcd2(x, y, i) → if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i)) [1]
if1(true, b1, b2, b3, x, y, i) → pair(result(y), neededIterations(i)) [1]
if1(false, b1, b2, b3, x, y, i) → if2(b1, b2, b3, x, y, i) [1]
if2(true, b2, b3, x, y, i) → pair(result(x), neededIterations(i)) [1]
if2(false, b2, b3, x, y, i) → if3(b2, b3, x, y, i) [1]
if3(false, b3, x, y, i) → gcd2(minus(x, y), y, i) [1]
if3(true, b3, x, y, i) → if4(b3, x, y, i) [1]
if4(false, x, y, i) → gcd2(x, minus(y, x), i) [1]
if4(true, x, y, i) → pair(result(x), neededIterations(i)) [1]
inc(0) → 0 [1]
inc(s(i)) → s(inc(i)) [1]
le(s(x), 0) → false [1]
le(0, y) → true [1]
le(s(x), s(y)) → le(x, y) [1]
minus(x, 0) → x [1]
minus(0, y) → 0 [1]
minus(s(x), s(y)) → minus(x, y) [1]
a → b [1]
a → c [1]
| gcd :: 0:s → 0:s → pair gcd2 :: 0:s → 0:s → 0:s → pair 0 :: 0:s if1 :: true:false → true:false → true:false → true:false → 0:s → 0:s → 0:s → pair le :: 0:s → 0:s → true:false inc :: 0:s → 0:s true :: true:false pair :: result → neededIterations → pair result :: 0:s → result neededIterations :: 0:s → neededIterations false :: true:false if2 :: true:false → true:false → true:false → 0:s → 0:s → 0:s → pair if3 :: true:false → true:false → 0:s → 0:s → 0:s → pair minus :: 0:s → 0:s → 0:s if4 :: true:false → 0:s → 0:s → 0:s → pair s :: 0:s → 0:s a :: b:c b :: b:c c :: b:c |
const, const1, const2
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 1
false => 0
b => 0
c => 1
const => 0
const1 => 0
const2 => 0
a -{ 1 }→ 1 :|:
a -{ 1 }→ 0 :|:
gcd(z, z') -{ 1 }→ gcd2(x, y, 0) :|: x >= 0, y >= 0, z = x, z' = y
gcd2(z, z', z'') -{ 1 }→ if1(le(x, 0), le(y, 0), le(x, y), le(y, x), x, y, inc(i)) :|: z'' = i, x >= 0, y >= 0, i >= 0, z = x, z' = y
if1(z, z', z'', z1, z2, z3, z4) -{ 1 }→ if2(b1, b2, b3, x, y, i) :|: z2 = x, b1 >= 0, z1 = b3, z3 = y, y >= 0, z4 = i, i >= 0, z' = b1, z = 0, z'' = b2, b3 >= 0, b2 >= 0, x >= 0
if1(z, z', z'', z1, z2, z3, z4) -{ 1 }→ 1 + (1 + y) + (1 + i) :|: z2 = x, b1 >= 0, z = 1, z1 = b3, z3 = y, y >= 0, z4 = i, i >= 0, z' = b1, z'' = b2, b3 >= 0, b2 >= 0, x >= 0
if2(z, z', z'', z1, z2, z3) -{ 1 }→ if3(b2, b3, x, y, i) :|: b2 >= 0, z2 = y, z3 = i, x >= 0, y >= 0, i >= 0, z' = b2, z = 0, z'' = b3, z1 = x, b3 >= 0
if2(z, z', z'', z1, z2, z3) -{ 1 }→ 1 + (1 + x) + (1 + i) :|: b2 >= 0, z2 = y, z = 1, z3 = i, x >= 0, y >= 0, i >= 0, z' = b2, z'' = b3, z1 = x, b3 >= 0
if3(z, z', z'', z1, z2) -{ 1 }→ if4(b3, x, y, i) :|: z1 = y, z2 = i, z' = b3, z = 1, x >= 0, y >= 0, i >= 0, z'' = x, b3 >= 0
if3(z, z', z'', z1, z2) -{ 1 }→ gcd2(minus(x, y), y, i) :|: z1 = y, z2 = i, z' = b3, x >= 0, y >= 0, i >= 0, z'' = x, z = 0, b3 >= 0
if4(z, z', z'', z1) -{ 1 }→ gcd2(x, minus(y, x), i) :|: z' = x, z'' = y, x >= 0, y >= 0, i >= 0, z = 0, z1 = i
if4(z, z', z'', z1) -{ 1 }→ 1 + (1 + x) + (1 + i) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0, i >= 0, z1 = i
inc(z) -{ 1 }→ 0 :|: z = 0
inc(z) -{ 1 }→ 1 + inc(i) :|: z = 1 + i, i >= 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 1 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 0 :|: x >= 0, z = 1 + x, z' = 0
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
| eq(start(V, V1, V4, V8, V9, V10, V11),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[gcd2(V, V1, V4, Out)],[V >= 0,V1 >= 0,V4 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[if1(V, V1, V4, V8, V9, V10, V11, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0,V10 >= 0,V11 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[if2(V, V1, V4, V8, V9, V10, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[if3(V, V1, V4, V8, V9, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0,V9 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[if4(V, V1, V4, V8, Out)],[V >= 0,V1 >= 0,V4 >= 0,V8 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[inc(V, Out)],[V >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V4, V8, V9, V10, V11),0,[a(Out)],[]). eq(gcd(V, V1, Out),1,[gcd2(V2, V3, 0, Ret)],[Out = Ret,V2 >= 0,V3 >= 0,V = V2,V1 = V3]). eq(gcd2(V, V1, V4, Out),1,[le(V5, 0, Ret0),le(V6, 0, Ret1),le(V5, V6, Ret2),le(V6, V5, Ret3),inc(V7, Ret6),if1(Ret0, Ret1, Ret2, Ret3, V5, V6, Ret6, Ret4)],[Out = Ret4,V4 = V7,V5 >= 0,V6 >= 0,V7 >= 0,V = V5,V1 = V6]). eq(if1(V, V1, V4, V8, V9, V10, V11, Out),1,[],[Out = 3 + V12 + V13,V9 = V14,V15 >= 0,V = 1,V8 = V16,V10 = V12,V12 >= 0,V11 = V13,V13 >= 0,V1 = V15,V4 = V17,V16 >= 0,V17 >= 0,V14 >= 0]). eq(if1(V, V1, V4, V8, V9, V10, V11, Out),1,[if2(V18, V19, V20, V21, V22, V23, Ret5)],[Out = Ret5,V9 = V21,V18 >= 0,V8 = V20,V10 = V22,V22 >= 0,V11 = V23,V23 >= 0,V1 = V18,V = 0,V4 = V19,V20 >= 0,V19 >= 0,V21 >= 0]). eq(if2(V, V1, V4, V8, V9, V10, Out),1,[],[Out = 3 + V24 + V25,V26 >= 0,V9 = V27,V = 1,V10 = V25,V24 >= 0,V27 >= 0,V25 >= 0,V1 = V26,V4 = V28,V8 = V24,V28 >= 0]). eq(if2(V, V1, V4, V8, V9, V10, Out),1,[if3(V29, V30, V31, V32, V33, Ret7)],[Out = Ret7,V29 >= 0,V9 = V32,V10 = V33,V31 >= 0,V32 >= 0,V33 >= 0,V1 = V29,V = 0,V4 = V30,V8 = V31,V30 >= 0]). eq(if3(V, V1, V4, V8, V9, Out),1,[minus(V34, V35, Ret01),gcd2(Ret01, V35, V36, Ret8)],[Out = Ret8,V8 = V35,V9 = V36,V1 = V37,V34 >= 0,V35 >= 0,V36 >= 0,V4 = V34,V = 0,V37 >= 0]). eq(if3(V, V1, V4, V8, V9, Out),1,[if4(V38, V39, V40, V41, Ret9)],[Out = Ret9,V8 = V40,V9 = V41,V1 = V38,V = 1,V39 >= 0,V40 >= 0,V41 >= 0,V4 = V39,V38 >= 0]). eq(if4(V, V1, V4, V8, Out),1,[minus(V43, V42, Ret11),gcd2(V42, Ret11, V44, Ret10)],[Out = Ret10,V1 = V42,V4 = V43,V42 >= 0,V43 >= 0,V44 >= 0,V = 0,V8 = V44]). eq(if4(V, V1, V4, V8, Out),1,[],[Out = 3 + V45 + V46,V1 = V45,V4 = V47,V = 1,V45 >= 0,V47 >= 0,V46 >= 0,V8 = V46]). eq(inc(V, Out),1,[],[Out = 0,V = 0]). eq(inc(V, Out),1,[inc(V48, Ret12)],[Out = 1 + Ret12,V = 1 + V48,V48 >= 0]). eq(le(V, V1, Out),1,[],[Out = 0,V49 >= 0,V = 1 + V49,V1 = 0]). eq(le(V, V1, Out),1,[],[Out = 1,V50 >= 0,V = 0,V1 = V50]). eq(le(V, V1, Out),1,[le(V51, V52, Ret13)],[Out = Ret13,V1 = 1 + V52,V51 >= 0,V52 >= 0,V = 1 + V51]). eq(minus(V, V1, Out),1,[],[Out = V53,V53 >= 0,V = V53,V1 = 0]). eq(minus(V, V1, Out),1,[],[Out = 0,V54 >= 0,V = 0,V1 = V54]). eq(minus(V, V1, Out),1,[minus(V55, V56, Ret14)],[Out = Ret14,V1 = 1 + V56,V55 >= 0,V56 >= 0,V = 1 + V55]). eq(a(Out),1,[],[Out = 0]). eq(a(Out),1,[],[Out = 1]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(gcd2(V,V1,V4,Out),[V,V1,V4],[Out]). input_output_vars(if1(V,V1,V4,V8,V9,V10,V11,Out),[V,V1,V4,V8,V9,V10,V11],[Out]). input_output_vars(if2(V,V1,V4,V8,V9,V10,Out),[V,V1,V4,V8,V9,V10],[Out]). input_output_vars(if3(V,V1,V4,V8,V9,Out),[V,V1,V4,V8,V9],[Out]). input_output_vars(if4(V,V1,V4,V8,Out),[V,V1,V4,V8],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(a(Out),[],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [a/1]
1. recursive : [minus/3]
2. recursive : [inc/2]
3. recursive : [le/3]
4. recursive : [gcd2/4,if1/8,if2/7,if3/6,if4/5]
5. non_recursive : [gcd/3]
6. non_recursive : [start/7]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into a/1
1. SCC is partially evaluated into minus/3
2. SCC is partially evaluated into inc/2
3. SCC is partially evaluated into le/3
4. SCC is partially evaluated into gcd2/4
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into start/7
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations a/1
* CE 34 is refined into CE [35]
* CE 33 is refined into CE [36]
### Cost equations --> "Loop" of a/1
* CEs [35] --> Loop 16
* CEs [36] --> Loop 17
### Ranking functions of CR a(Out)
#### Partial ranking functions of CR a(Out)
### Specialization of cost equations minus/3
* CE 22 is refined into CE [37]
* CE 20 is refined into CE [38]
* CE 21 is refined into CE [39]
### Cost equations --> "Loop" of minus/3
* CEs [38] --> Loop 18
* CEs [39] --> Loop 19
* CEs [37] --> Loop 20
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [20]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1
### Specialization of cost equations inc/2
* CE 29 is refined into CE [40]
* CE 28 is refined into CE [41]
### Cost equations --> "Loop" of inc/2
* CEs [41] --> Loop 21
* CEs [40] --> Loop 22
### Ranking functions of CR inc(V,Out)
* RF of phase [22]: [V]
#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
### Specialization of cost equations le/3
* CE 32 is refined into CE [42]
* CE 30 is refined into CE [43]
* CE 31 is refined into CE [44]
### Cost equations --> "Loop" of le/3
* CEs [43] --> Loop 23
* CEs [44] --> Loop 24
* CEs [42] --> Loop 25
### Ranking functions of CR le(V,V1,Out)
* RF of phase [25]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V1
### Specialization of cost equations gcd2/4
* CE 26 is refined into CE [45,46,47,48]
* CE 25 is refined into CE [49,50]
* CE 27 is refined into CE [51,52]
* CE 23 is refined into CE [53,54]
* CE 24 is refined into CE [55,56]
### Cost equations --> "Loop" of gcd2/4
* CEs [54] --> Loop 26
* CEs [56] --> Loop 27
* CEs [53] --> Loop 28
* CEs [55] --> Loop 29
* CEs [50] --> Loop 30
* CEs [49] --> Loop 31
* CEs [52] --> Loop 32
* CEs [51] --> Loop 33
* CEs [48] --> Loop 34
* CEs [47] --> Loop 35
* CEs [46] --> Loop 36
* CEs [45] --> Loop 37
### Ranking functions of CR gcd2(V,V1,V4,Out)
* RF of phase [26,27]: [V+V1-2]
* RF of phase [28,29]: [V+V1-2]
#### Partial ranking functions of CR gcd2(V,V1,V4,Out)
* Partial RF of phase [26,27]:
- RF of loop [26:1]:
V-1
V-V1 depends on loops [27:1]
- RF of loop [27:1]:
-V+V1 depends on loops [26:1]
V1-1
* Partial RF of phase [28,29]:
- RF of loop [28:1]:
V-1
V-V1 depends on loops [29:1]
- RF of loop [29:1]:
-V+V1 depends on loops [28:1]
V1-1
### Specialization of cost equations start/7
* CE 2 is refined into CE [57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72]
* CE 3 is refined into CE [73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88]
* CE 4 is refined into CE [89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104]
* CE 5 is refined into CE [105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120]
* CE 6 is refined into CE [121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136]
* CE 7 is refined into CE [137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152]
* CE 8 is refined into CE [153]
* CE 9 is refined into CE [154]
* CE 10 is refined into CE [155]
* CE 11 is refined into CE [156]
* CE 12 is refined into CE [157]
* CE 13 is refined into CE [158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173]
* CE 14 is refined into CE [174,175,176,177,178]
* CE 15 is refined into CE [179,180,181,182,183,184,185,186,187,188]
* CE 16 is refined into CE [189,190]
* CE 17 is refined into CE [191,192,193,194]
* CE 18 is refined into CE [195,196,197,198]
* CE 19 is refined into CE [199,200]
### Cost equations --> "Loop" of start/7
* CEs [57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200] --> Loop 38
### Ranking functions of CR start(V,V1,V4,V8,V9,V10,V11)
#### Partial ranking functions of CR start(V,V1,V4,V8,V9,V10,V11)
Computing Bounds
=====================================
#### Cost of chains of a(Out):
* Chain [17]: 1
with precondition: [Out=0]
* Chain [16]: 1
with precondition: [Out=1]
#### Cost of chains of minus(V,V1,Out):
* Chain [[20],19]: 1*it(20)+1
Such that:it(20) =< V
with precondition: [Out=0,V>=1,V1>=V]
* Chain [[20],18]: 1*it(20)+1
Such that:it(20) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [19]: 1
with precondition: [V=0,Out=0,V1>=0]
* Chain [18]: 1
with precondition: [V1=0,V=Out,V>=0]
#### Cost of chains of inc(V,Out):
* Chain [[22],21]: 1*it(22)+1
Such that:it(22) =< Out
with precondition: [V=Out,V>=1]
* Chain [21]: 1
with precondition: [V=0,Out=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[25],24]: 1*it(25)+1
Such that:it(25) =< V
with precondition: [Out=1,V>=1,V1>=V]
* Chain [[25],23]: 1*it(25)+1
Such that:it(25) =< V1
with precondition: [Out=0,V1>=1,V>=V1+1]
* Chain [24]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [23]: 1
with precondition: [V1=0,Out=0,V>=1]
#### Cost of chains of gcd2(V,V1,V4,Out):
* Chain [[28,29],31]: 10*it(28)+11*it(29)+2*s(1)+3*s(13)+3*s(15)+10
Such that:aux(7) =< -V+V1
aux(8) =< V
aux(5) =< V-V1
aux(9) =< V+V1
aux(10) =< V+V1-2*Out+6
aux(11) =< V-Out+3
aux(12) =< V1
aux(13) =< V1-Out+3
aux(1) =< Out
s(1) =< aux(1)
aux(6) =< aux(8)
it(28) =< aux(8)
it(28) =< aux(9)
it(29) =< aux(9)
it(28) =< aux(10)
it(29) =< aux(10)
aux(6) =< aux(11)
it(28) =< aux(11)
aux(4) =< aux(12)
it(29) =< aux(12)
aux(4) =< aux(13)
it(29) =< aux(13)
it(29) =< aux(6)+aux(7)
it(28) =< aux(4)+aux(5)
s(15) =< aux(4)
s(13) =< aux(6)
with precondition: [V4=0,Out>=4,V+3>=Out,V1+3>=Out,V+V1+9>=3*Out]
* Chain [[26,27],30]: 10*it(26)+11*it(27)+2*s(17)+1*s(19)+3*s(34)+1*s(35)+3*s(37)+1*s(38)+10
Such that:aux(21) =< -V+V1
aux(23) =< V
aux(18) =< V-V1
aux(24) =< V+V1
aux(25) =< V+V1+2*V4-2*Out+6
aux(26) =< V+V4-Out+3
aux(27) =< V1
aux(28) =< V1+V4-Out+3
aux(14) =< -V4+Out
aux(29) =< V4
s(19) =< aux(29)
s(17) =< aux(14)
aux(20) =< aux(23)
it(26) =< aux(23)
it(26) =< aux(24)
it(27) =< aux(24)
it(26) =< aux(25)
it(27) =< aux(25)
aux(20) =< aux(26)
it(26) =< aux(26)
aux(17) =< aux(27)
it(27) =< aux(27)
aux(17) =< aux(28)
it(27) =< aux(28)
aux(22) =< aux(29)
it(27) =< aux(20)+aux(21)
it(26) =< aux(17)+aux(18)
s(38) =< it(27)*aux(22)
s(35) =< it(26)*aux(29)
s(37) =< aux(17)
s(34) =< aux(20)
with precondition: [V4>=1,Out>=V4+4,V+V4+3>=Out,V1+V4+3>=Out,V+V1+3*V4+9>=3*Out]
* Chain [37]: 7
with precondition: [V=0,V1=0,V4=0,Out=3]
* Chain [36]: 1*s(40)+7
Such that:s(40) =< V4
with precondition: [V=0,V1=0,V4+3=Out,V4>=1]
* Chain [35]: 7
with precondition: [V=0,V4=0,V1+3=Out,V1>=1]
* Chain [34]: 1*s(41)+7
Such that:s(41) =< V4
with precondition: [V=0,V1+V4+3=Out,V1>=1,V4>=1]
* Chain [33]: 8
with precondition: [V1=0,V4=0,V+3=Out,V>=1]
* Chain [32]: 1*s(42)+8
Such that:s(42) =< V4
with precondition: [V1=0,V+V4+3=Out,V>=1,V4>=1]
* Chain [31]: 2*s(1)+10
Such that:aux(1) =< V1
s(1) =< aux(1)
with precondition: [V4=0,V=V1,V+3=Out,V>=1]
* Chain [30]: 2*s(17)+1*s(19)+10
Such that:s(19) =< V4
aux(14) =< V
s(17) =< aux(14)
with precondition: [V=V1,V+V4+3=Out,V>=1,V4>=1]
#### Cost of chains of start(V,V1,V4,V8,V9,V10,V11):
* Chain [38]: 16*s(43)+34*s(47)+27*s(50)+4*s(66)+20*s(68)+22*s(69)+6*s(71)+6*s(72)+1*s(95)+1*s(96)+26*s(103)+4*s(122)+20*s(124)+22*s(125)+12*s(127)+6*s(128)+1*s(151)+1*s(152)+14*s(159)+4*s(178)+20*s(180)+22*s(181)+12*s(183)+6*s(184)+1*s(207)+1*s(208)+6*s(221)+4*s(234)+20*s(236)+22*s(237)+6*s(239)+1*s(263)+1*s(264)+6*s(277)+4*s(290)+20*s(292)+22*s(293)+6*s(295)+1*s(319)+1*s(320)+6*s(333)+4*s(346)+20*s(348)+22*s(349)+6*s(351)+6*s(352)+1*s(375)+1*s(376)+10*s(386)+6*s(389)+4*s(402)+20*s(404)+22*s(405)+6*s(407)+15*s(408)+1*s(431)+1*s(432)+6*s(446)+30*s(448)+33*s(449)+9*s(452)+5*s(457)+1*s(494)+1*s(495)+15
Such that:aux(75) =< -V+V1
aux(76) =< V
aux(77) =< V+3
aux(78) =< V-V1
aux(79) =< V+V1
aux(80) =< V+V1+6
aux(81) =< -2*V1+V4
aux(82) =< -V1+V4
aux(83) =< -V1+V4+3
aux(84) =< V1
aux(85) =< V1+3
aux(86) =< 2*V1-V4
aux(87) =< -2*V4+V8
aux(88) =< -V4+V8
aux(89) =< -V4+V8+3
aux(90) =< -V4+2*V8
aux(91) =< V4
aux(92) =< V4+3
aux(93) =< V4+6
aux(94) =< V4-2*V8
aux(95) =< V4-V8
aux(96) =< V4-V8+3
aux(97) =< 2*V4-V8
aux(98) =< V4/2
aux(99) =< -2*V8+V9
aux(100) =< -V8+V9
aux(101) =< -V8+V9+3
aux(102) =< -V8+2*V9
aux(103) =< V8
aux(104) =< V8+3
aux(105) =< V8+6
aux(106) =< V8-2*V9
aux(107) =< V8-V9
aux(108) =< V8-V9+3
aux(109) =< 2*V8-V9
aux(110) =< V8/2
aux(111) =< -2*V9+V10
aux(112) =< -V9+V10
aux(113) =< -V9+V10+3
aux(114) =< -V9+2*V10
aux(115) =< V9
aux(116) =< V9+3
aux(117) =< V9+6
aux(118) =< V9-2*V10
aux(119) =< V9-V10
aux(120) =< V9-V10+3
aux(121) =< 2*V9-V10
aux(122) =< V9/2
aux(123) =< V10
aux(124) =< V10+3
aux(125) =< V10+6
aux(126) =< V10/2
aux(127) =< V11
s(457) =< aux(76)
s(386) =< aux(84)
s(159) =< aux(91)
s(103) =< aux(103)
s(47) =< aux(115)
s(50) =< aux(123)
s(43) =< aux(127)
s(446) =< aux(85)
s(447) =< aux(76)
s(448) =< aux(76)
s(448) =< aux(79)
s(449) =< aux(79)
s(448) =< aux(80)
s(449) =< aux(80)
s(447) =< aux(77)
s(448) =< aux(77)
s(403) =< aux(84)
s(449) =< aux(84)
s(403) =< aux(85)
s(449) =< aux(85)
s(449) =< s(447)+aux(75)
s(448) =< s(403)+aux(78)
s(408) =< s(403)
s(452) =< s(447)
s(493) =< aux(91)
s(494) =< s(449)*s(493)
s(495) =< s(448)*aux(91)
s(402) =< aux(83)
s(404) =< aux(84)
s(404) =< aux(91)
s(405) =< aux(91)
s(404) =< aux(93)
s(405) =< aux(93)
s(404) =< aux(85)
s(406) =< aux(82)
s(405) =< aux(82)
s(406) =< aux(83)
s(405) =< aux(83)
s(405) =< s(403)+aux(81)
s(404) =< s(406)+aux(86)
s(407) =< s(406)
s(430) =< aux(103)
s(431) =< s(405)*s(430)
s(432) =< s(404)*aux(103)
s(346) =< aux(89)
s(347) =< aux(91)
s(348) =< aux(91)
s(348) =< aux(103)
s(349) =< aux(103)
s(348) =< aux(105)
s(349) =< aux(105)
s(347) =< aux(92)
s(348) =< aux(92)
s(350) =< aux(88)
s(349) =< aux(88)
s(350) =< aux(89)
s(349) =< aux(89)
s(349) =< s(347)+aux(87)
s(348) =< s(350)+aux(97)
s(351) =< s(350)
s(352) =< s(347)
s(206) =< aux(115)
s(375) =< s(349)*s(206)
s(376) =< s(348)*aux(115)
s(178) =< aux(104)
s(179) =< aux(95)
s(180) =< aux(95)
s(180) =< aux(91)
s(181) =< aux(91)
s(180) =< aux(93)
s(181) =< aux(93)
s(179) =< aux(96)
s(180) =< aux(96)
s(182) =< aux(103)
s(181) =< aux(103)
s(182) =< aux(104)
s(181) =< aux(104)
s(181) =< s(179)+aux(90)
s(180) =< s(182)+aux(94)
s(183) =< s(182)
s(184) =< s(179)
s(207) =< s(181)*s(206)
s(208) =< s(180)*aux(115)
s(389) =< aux(98)
s(290) =< aux(101)
s(292) =< aux(103)
s(292) =< aux(115)
s(293) =< aux(115)
s(292) =< aux(117)
s(293) =< aux(117)
s(292) =< aux(104)
s(294) =< aux(100)
s(293) =< aux(100)
s(294) =< aux(101)
s(293) =< aux(101)
s(293) =< s(182)+aux(99)
s(292) =< s(294)+aux(109)
s(295) =< s(294)
s(150) =< aux(123)
s(319) =< s(293)*s(150)
s(320) =< s(292)*aux(123)
s(122) =< aux(116)
s(123) =< aux(107)
s(124) =< aux(107)
s(124) =< aux(103)
s(125) =< aux(103)
s(124) =< aux(105)
s(125) =< aux(105)
s(123) =< aux(108)
s(124) =< aux(108)
s(126) =< aux(115)
s(125) =< aux(115)
s(126) =< aux(116)
s(125) =< aux(116)
s(125) =< s(123)+aux(102)
s(124) =< s(126)+aux(106)
s(127) =< s(126)
s(128) =< s(123)
s(151) =< s(125)*s(150)
s(152) =< s(124)*aux(123)
s(333) =< aux(110)
s(234) =< aux(113)
s(236) =< aux(115)
s(236) =< aux(123)
s(237) =< aux(123)
s(236) =< aux(125)
s(237) =< aux(125)
s(236) =< aux(116)
s(238) =< aux(112)
s(237) =< aux(112)
s(238) =< aux(113)
s(237) =< aux(113)
s(237) =< s(126)+aux(111)
s(236) =< s(238)+aux(121)
s(239) =< s(238)
s(94) =< aux(127)
s(263) =< s(237)*s(94)
s(264) =< s(236)*aux(127)
s(66) =< aux(124)
s(67) =< aux(119)
s(68) =< aux(119)
s(68) =< aux(115)
s(69) =< aux(115)
s(68) =< aux(117)
s(69) =< aux(117)
s(67) =< aux(120)
s(68) =< aux(120)
s(70) =< aux(123)
s(69) =< aux(123)
s(70) =< aux(124)
s(69) =< aux(124)
s(69) =< s(67)+aux(114)
s(68) =< s(70)+aux(118)
s(71) =< s(70)
s(72) =< s(67)
s(95) =< s(69)*s(94)
s(96) =< s(68)*aux(127)
s(277) =< aux(122)
s(221) =< aux(126)
with precondition: []
Closed-form bounds of start(V,V1,V4,V8,V9,V10,V11):
-------------------------------------
* Chain [38] with precondition: []
- Upper bound: nat(V)*44+15+nat(V1)*45+nat(V4)*84+nat(V4)*nat(V)+nat(V+V1)*nat(V4)+nat(V8)*102+nat(V8)*nat(V1)+nat(V8)*nat(V4)+nat(V9)*110+nat(V9)*2*nat(V4)+nat(V9)*nat(V8)+nat(V4-V8)*nat(V9)+nat(V10)*55+nat(V10)*2*nat(V8)+nat(V10)*nat(V9)+nat(V8-V9)*nat(V10)+nat(V11)*16+nat(V11)*2*nat(V9)+nat(V11)*nat(V10)+nat(V9-V10)*nat(V11)+nat(V+V1)*33+nat(V1+3)*6+nat(V8+3)*4+nat(V9+3)*4+nat(V10+3)*4+nat(-V1+V4)*6+nat(-V4+V8)*6+nat(-V8+V9)*6+nat(-V9+V10)*6+nat(-V1+V4+3)*4+nat(-V4+V8+3)*4+nat(-V8+V9+3)*4+nat(-V9+V10+3)*4+nat(V4-V8)*26+nat(V8-V9)*26+nat(V9-V10)*26+nat(V4/2)*6+nat(V8/2)*6+nat(V9/2)*6+nat(V10/2)*6
- Complexity: n^2
### Maximum cost of start(V,V1,V4,V8,V9,V10,V11): nat(V)*44+15+nat(V1)*45+nat(V4)*84+nat(V4)*nat(V)+nat(V+V1)*nat(V4)+nat(V8)*102+nat(V8)*nat(V1)+nat(V8)*nat(V4)+nat(V9)*110+nat(V9)*2*nat(V4)+nat(V9)*nat(V8)+nat(V4-V8)*nat(V9)+nat(V10)*55+nat(V10)*2*nat(V8)+nat(V10)*nat(V9)+nat(V8-V9)*nat(V10)+nat(V11)*16+nat(V11)*2*nat(V9)+nat(V11)*nat(V10)+nat(V9-V10)*nat(V11)+nat(V+V1)*33+nat(V1+3)*6+nat(V8+3)*4+nat(V9+3)*4+nat(V10+3)*4+nat(-V1+V4)*6+nat(-V4+V8)*6+nat(-V8+V9)*6+nat(-V9+V10)*6+nat(-V1+V4+3)*4+nat(-V4+V8+3)*4+nat(-V8+V9+3)*4+nat(-V9+V10+3)*4+nat(V4-V8)*26+nat(V8-V9)*26+nat(V9-V10)*26+nat(V4/2)*6+nat(V8/2)*6+nat(V9/2)*6+nat(V10/2)*6
Asymptotic class: n^2
* Total analysis performed in 3248 ms.